'''
Created on 2011-09-08

@author: kacper
'''
import unittest
from dataStructs.formulaSet import Theory
from parsing.parser import sents_parse_string
from dataStructs.definitions import Const



class Test(unittest.TestCase):


    def setUp(self):
        pass


    def tearDown(self):
        pass


    def checkTypes(self):        
        fo1 = sents_parse_string("a || b || a || c")[0]
        lst = fo1.getConsts()
        typesDiffrentThenCont =  filter(lambda x: x._class__!= Const, lst)
        self.assertTrue(len(typesDiffrentThenCont)==0)

    def testSimpeGet(self):
        fo1 = sents_parse_string("a || b || a || c")[0]
        lst = fo1.getConsts()
        self.assertEqual(3,len(lst))
        self.assertTrue(Const('a') in lst)
        self.assertTrue(Const("b") in lst)
        self.assertTrue(Const("c") in lst)

    def testGetConstFromRel(self):
        fo1 = sents_parse_string("r(a, b , a , c)")[0]
        lst = fo1.getConsts()
        self.assertEqual(4,len(lst))
        self.assertTrue(Const('a') in lst)
        self.assertTrue(Const("b") in lst)
        self.assertTrue(Const("c") in lst)


    def testgetFromComplex(self):
        th = Theory()
        fo1 = sents_parse_string("a&&d->c->a||r(a, b , a , c)")[0]
        lst = fo1.getConsts()
        self.assertEqual(4,len(lst))
        self.assertTrue(Const('a') in lst)
        self.assertTrue(Const("b") in lst)
        self.assertTrue(Const("c") in lst)
        self.assertTrue(Const("d") in lst)


if __name__ == "__main__":
    #import sys;sys.argv = ['', 'Test.testSimpeGet']
    unittest.main()